Nuprl Definition : es-change-to 11,40

@e(xv)
== es-dtype(es; loc(e); xT) c (((es-when(esxe) = v))  (es-after(esxe) = v)) 
latex



clarification:

es-change-to(es;T;x;e;v)
== es-dtype(es; es-loc(ese); xT)
== c (((es-when(esxe) = v  T))  (es-after(esxe) = v  T)) 
latex


DefinitionsA c B, es-dtype(esixT), loc(e), P  Q, A, es-when(esxe), s = t, es-after(esxe)
FDL editor aliaseses-change-to

origin